YES 3.458 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ LR

mainModule List
  ((elemIndices :: (Eq a, Eq b) => (a,b ->  [(a,b)]  ->  [Int]) :: (Eq b, Eq a) => (a,b ->  [(a,b)]  ->  [Int])

module List where
  import qualified Maybe
import qualified Prelude

  elemIndices :: Eq a => a  ->  [a ->  [Int]
elemIndices x findIndices (== x)

  findIndices :: (a  ->  Bool ->  [a ->  [Int]
findIndices p xs concatMap (\vv1 ->
case vv1 of
  (x,i)->  if p x then i : [] else []
  _-> []
) (zip xs (enumFrom 0))


module Maybe where
  import qualified List
import qualified Prelude



Lambda Reductions:
The following Lambda expression
\vv1
case vv1 of
 (x,i) → if p x then i : [] else []
 _ → []

is transformed to
findIndices0 p vv1 = 
case vv1 of
 (x,i) → if p x then i : [] else []
 _ → []

The following Lambda expression
\ab→(a,b)

is transformed to
zip0 a b = (a,b)



↳ HASKELL
  ↳ LR
HASKELL
      ↳ CR

mainModule List
  ((elemIndices :: (Eq a, Eq b) => (b,a ->  [(b,a)]  ->  [Int]) :: (Eq a, Eq b) => (b,a ->  [(b,a)]  ->  [Int])

module List where
  import qualified Maybe
import qualified Prelude

  elemIndices :: Eq a => a  ->  [a ->  [Int]
elemIndices x findIndices (== x)

  findIndices :: (a  ->  Bool ->  [a ->  [Int]
findIndices p xs concatMap (findIndices0 p) (zip xs (enumFrom 0))

  
findIndices0 p vv1 
case vv1 of
  (x,i)->  if p x then i : [] else []
  _-> []


module Maybe where
  import qualified List
import qualified Prelude



Case Reductions:
The following Case expression
case vv1 of
 (x,i) → if p x then i : [] else []
 _ → []

is transformed to
findIndices00 p (x,i) = if p x then i : [] else []
findIndices00 p _ = []



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
HASKELL
          ↳ IFR

mainModule List
  ((elemIndices :: (Eq a, Eq b) => (a,b ->  [(a,b)]  ->  [Int]) :: (Eq b, Eq a) => (a,b ->  [(a,b)]  ->  [Int])

module List where
  import qualified Maybe
import qualified Prelude

  elemIndices :: Eq a => a  ->  [a ->  [Int]
elemIndices x findIndices (== x)

  findIndices :: (a  ->  Bool ->  [a ->  [Int]
findIndices p xs concatMap (findIndices0 p) (zip xs (enumFrom 0))

  
findIndices0 p vv1 findIndices00 p vv1

  
findIndices00 p (x,i if p x then i : [] else []
findIndices00 p _ []


module Maybe where
  import qualified List
import qualified Prelude



If Reductions:
The following If expression
if p x then i : [] else []

is transformed to
findIndices000 i True = i : []
findIndices000 i False = []



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
HASKELL
              ↳ BR

mainModule List
  ((elemIndices :: (Eq b, Eq a) => (a,b ->  [(a,b)]  ->  [Int]) :: (Eq b, Eq a) => (a,b ->  [(a,b)]  ->  [Int])

module List where
  import qualified Maybe
import qualified Prelude

  elemIndices :: Eq a => a  ->  [a ->  [Int]
elemIndices x findIndices (== x)

  findIndices :: (a  ->  Bool ->  [a ->  [Int]
findIndices p xs concatMap (findIndices0 p) (zip xs (enumFrom 0))

  
findIndices0 p vv1 findIndices00 p vv1

  
findIndices00 p (x,ifindIndices000 i (p x)
findIndices00 p _ []

  
findIndices000 i True i : []
findIndices000 i False []


module Maybe where
  import qualified List
import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
HASKELL
                  ↳ COR

mainModule List
  ((elemIndices :: (Eq b, Eq a) => (b,a ->  [(b,a)]  ->  [Int]) :: (Eq b, Eq a) => (b,a ->  [(b,a)]  ->  [Int])

module List where
  import qualified Maybe
import qualified Prelude

  elemIndices :: Eq a => a  ->  [a ->  [Int]
elemIndices x findIndices (== x)

  findIndices :: (a  ->  Bool ->  [a ->  [Int]
findIndices p xs concatMap (findIndices0 p) (zip xs (enumFrom 0))

  
findIndices0 p vv1 findIndices00 p vv1

  
findIndices00 p (x,ifindIndices000 i (p x)
findIndices00 p vw []

  
findIndices000 i True i : []
findIndices000 i False []


module Maybe where
  import qualified List
import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
HASKELL
                      ↳ NumRed

mainModule List
  ((elemIndices :: (Eq b, Eq a) => (b,a ->  [(b,a)]  ->  [Int]) :: (Eq a, Eq b) => (b,a ->  [(b,a)]  ->  [Int])

module List where
  import qualified Maybe
import qualified Prelude

  elemIndices :: Eq a => a  ->  [a ->  [Int]
elemIndices x findIndices (== x)

  findIndices :: (a  ->  Bool ->  [a ->  [Int]
findIndices p xs concatMap (findIndices0 p) (zip xs (enumFrom 0))

  
findIndices0 p vv1 findIndices00 p vv1

  
findIndices00 p (x,ifindIndices000 i (p x)
findIndices00 p vw []

  
findIndices000 i True i : []
findIndices000 i False []


module Maybe where
  import qualified List
import qualified Prelude



Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
HASKELL
                          ↳ Narrow

mainModule List
  (elemIndices :: (Eq a, Eq b) => (a,b ->  [(a,b)]  ->  [Int])

module List where
  import qualified Maybe
import qualified Prelude

  elemIndices :: Eq a => a  ->  [a ->  [Int]
elemIndices x findIndices (== x)

  findIndices :: (a  ->  Bool ->  [a ->  [Int]
findIndices p xs concatMap (findIndices0 p) (zip xs (enumFrom (Pos Zero)))

  
findIndices0 p vv1 findIndices00 p vv1

  
findIndices00 p (x,ifindIndices000 i (p x)
findIndices00 p vw []

  
findIndices000 i True i : []
findIndices000 i False []


module Maybe where
  import qualified List
import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primEqNat(Succ(yu3000), Succ(yu4110000)) → new_primEqNat(yu3000, yu4110000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(yu10400), Succ(yu411001000)) → new_primPlusNat(yu10400, yu411001000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(yu30100), Succ(yu41100100)) → new_primMulNat(yu30100, Succ(yu41100100))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_esEs3(Right(yu300), Right(yu411000), bdb, app(app(ty_@2, bdh), bea)) → new_esEs2(yu300, yu411000, bdh, bea)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), app(ty_[], da), cc, cd) → new_esEs1(yu300, yu411000, da)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), df, cc, app(app(ty_Either, fh), ga)) → new_esEs3(yu302, yu411002, fh, ga)
new_esEs2(@2(yu300, yu301), @2(yu411000, yu411001), baf, app(app(ty_@2, bbd), bbe)) → new_esEs2(yu301, yu411001, bbd, bbe)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), df, app(app(ty_@2, ed), ee), cd) → new_esEs2(yu301, yu411001, ed, ee)
new_esEs2(@2(yu300, yu301), @2(yu411000, yu411001), baf, app(ty_Maybe, bag)) → new_esEs(yu301, yu411001, bag)
new_esEs(Just(yu300), Just(yu411000), app(app(app(ty_@3, bb), bc), bd)) → new_esEs0(yu300, yu411000, bb, bc, bd)
new_esEs2(@2(yu300, yu301), @2(yu411000, yu411001), app(ty_Maybe, hd), he) → new_esEs(yu300, yu411000, hd)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), df, app(ty_[], ec), cd) → new_esEs1(yu301, yu411001, ec)
new_esEs3(Right(yu300), Right(yu411000), bdb, app(app(ty_Either, beb), bec)) → new_esEs3(yu300, yu411000, beb, bec)
new_esEs1(:(yu300, yu301), :(yu411000, yu411001), hc) → new_esEs1(yu301, yu411001, hc)
new_esEs2(@2(yu300, yu301), @2(yu411000, yu411001), app(app(ty_@2, bab), bac), he) → new_esEs2(yu300, yu411000, bab, bac)
new_esEs1(:(yu300, yu301), :(yu411000, yu411001), app(ty_[], gf)) → new_esEs1(yu300, yu411000, gf)
new_esEs(Just(yu300), Just(yu411000), app(ty_Maybe, ba)) → new_esEs(yu300, yu411000, ba)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), df, app(app(app(ty_@3, dh), ea), eb), cd) → new_esEs0(yu301, yu411001, dh, ea, eb)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), app(app(ty_@2, db), dc), cc, cd) → new_esEs2(yu300, yu411000, db, dc)
new_esEs3(Right(yu300), Right(yu411000), bdb, app(app(app(ty_@3, bdd), bde), bdf)) → new_esEs0(yu300, yu411000, bdd, bde, bdf)
new_esEs3(Left(yu300), Left(yu411000), app(app(ty_Either, bch), bda), bca) → new_esEs3(yu300, yu411000, bch, bda)
new_esEs2(@2(yu300, yu301), @2(yu411000, yu411001), app(ty_[], baa), he) → new_esEs1(yu300, yu411000, baa)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), df, cc, app(ty_[], fd)) → new_esEs1(yu302, yu411002, fd)
new_esEs1(:(yu300, yu301), :(yu411000, yu411001), app(app(ty_Either, ha), hb)) → new_esEs3(yu300, yu411000, ha, hb)
new_esEs3(Left(yu300), Left(yu411000), app(app(app(ty_@3, bcb), bcc), bcd), bca) → new_esEs0(yu300, yu411000, bcb, bcc, bcd)
new_esEs(Just(yu300), Just(yu411000), app(app(ty_@2, bf), bg)) → new_esEs2(yu300, yu411000, bf, bg)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), df, cc, app(app(ty_@2, ff), fg)) → new_esEs2(yu302, yu411002, ff, fg)
new_esEs3(Left(yu300), Left(yu411000), app(app(ty_@2, bcf), bcg), bca) → new_esEs2(yu300, yu411000, bcf, bcg)
new_esEs2(@2(yu300, yu301), @2(yu411000, yu411001), baf, app(app(app(ty_@3, bah), bba), bbb)) → new_esEs0(yu301, yu411001, bah, bba, bbb)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), df, cc, app(app(app(ty_@3, fa), fb), fc)) → new_esEs0(yu302, yu411002, fa, fb, fc)
new_esEs2(@2(yu300, yu301), @2(yu411000, yu411001), baf, app(app(ty_Either, bbf), bbg)) → new_esEs3(yu301, yu411001, bbf, bbg)
new_esEs1(:(yu300, yu301), :(yu411000, yu411001), app(ty_Maybe, gb)) → new_esEs(yu300, yu411000, gb)
new_esEs3(Right(yu300), Right(yu411000), bdb, app(ty_[], bdg)) → new_esEs1(yu300, yu411000, bdg)
new_esEs(Just(yu300), Just(yu411000), app(ty_[], be)) → new_esEs1(yu300, yu411000, be)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), app(app(ty_Either, dd), de), cc, cd) → new_esEs3(yu300, yu411000, dd, de)
new_esEs2(@2(yu300, yu301), @2(yu411000, yu411001), app(app(app(ty_@3, hf), hg), hh), he) → new_esEs0(yu300, yu411000, hf, hg, hh)
new_esEs(Just(yu300), Just(yu411000), app(app(ty_Either, bh), ca)) → new_esEs3(yu300, yu411000, bh, ca)
new_esEs3(Right(yu300), Right(yu411000), bdb, app(ty_Maybe, bdc)) → new_esEs(yu300, yu411000, bdc)
new_esEs1(:(yu300, yu301), :(yu411000, yu411001), app(app(app(ty_@3, gc), gd), ge)) → new_esEs0(yu300, yu411000, gc, gd, ge)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), df, app(ty_Maybe, dg), cd) → new_esEs(yu301, yu411001, dg)
new_esEs1(:(yu300, yu301), :(yu411000, yu411001), app(app(ty_@2, gg), gh)) → new_esEs2(yu300, yu411000, gg, gh)
new_esEs2(@2(yu300, yu301), @2(yu411000, yu411001), baf, app(ty_[], bbc)) → new_esEs1(yu301, yu411001, bbc)
new_esEs2(@2(yu300, yu301), @2(yu411000, yu411001), app(app(ty_Either, bad), bae), he) → new_esEs3(yu300, yu411000, bad, bae)
new_esEs3(Left(yu300), Left(yu411000), app(ty_[], bce), bca) → new_esEs1(yu300, yu411000, bce)
new_esEs3(Left(yu300), Left(yu411000), app(ty_Maybe, bbh), bca) → new_esEs(yu300, yu411000, bbh)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), df, cc, app(ty_Maybe, eh)) → new_esEs(yu302, yu411002, eh)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), df, app(app(ty_Either, ef), eg), cd) → new_esEs3(yu301, yu411001, ef, eg)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), app(ty_Maybe, cb), cc, cd) → new_esEs(yu300, yu411000, cb)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), app(app(app(ty_@3, ce), cf), cg), cc, cd) → new_esEs0(yu300, yu411000, ce, cf, cg)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_psPs(yu85, False, yu87, yu88, :(yu890, yu891), yu90, ba, bb) → new_foldr(@2(yu87, yu88), yu890, yu891, new_primPlusNat0(yu90, Zero), new_primPlusNat0(yu90, Zero), ba, bb)
new_foldr(@2(yu30, yu31), @2(yu41100, yu41101), yu4111, yu61, yu62, bc, bd) → new_psPs(yu61, new_asAs(new_esEs4(yu30, yu41100, bc), new_esEs5(yu31, yu41101, bd)), yu30, yu31, yu4111, yu62, bc, bd)
new_psPs(yu85, True, yu87, yu88, yu89, yu90, ba, bb) → new_psPs0(yu87, yu88, yu89, yu90, ba, bb)
new_psPs0(yu87, yu88, :(yu890, yu891), yu90, ba, bb) → new_foldr(@2(yu87, yu88), yu890, yu891, new_primPlusNat0(yu90, Zero), new_primPlusNat0(yu90, Zero), ba, bb)

The TRS R consists of the following rules:

new_esEs22(yu302, yu411002, ty_Integer) → new_esEs14(yu302, yu411002)
new_esEs7(Just(yu300), Just(yu411000), app(ty_Maybe, fd)) → new_esEs7(yu300, yu411000, fd)
new_esEs7(Just(yu300), Just(yu411000), app(ty_[], ga)) → new_esEs15(yu300, yu411000, ga)
new_esEs20(yu300, yu411000, app(ty_Maybe, gg)) → new_esEs7(yu300, yu411000, gg)
new_esEs25(yu300, yu411000, ty_Int) → new_esEs8(yu300, yu411000)
new_esEs22(yu302, yu411002, app(app(ty_@2, bbh), bca)) → new_esEs16(yu302, yu411002, bbh, bca)
new_esEs6(Left(yu300), Left(yu411000), app(app(ty_@2, cc), cd), bf) → new_esEs16(yu300, yu411000, cc, cd)
new_esEs6(Right(yu300), Right(yu411000), da, ty_Float) → new_esEs17(yu300, yu411000)
new_esEs27(yu300, yu411000, ty_Double) → new_esEs9(yu300, yu411000)
new_primPlusNat1(Succ(yu10400), Succ(yu411001000)) → Succ(Succ(new_primPlusNat1(yu10400, yu411001000)))
new_primEqInt(Pos(Succ(yu3000)), Neg(yu411000)) → False
new_primEqInt(Neg(Succ(yu3000)), Pos(yu411000)) → False
new_esEs7(Nothing, Just(yu411000), ed) → False
new_esEs7(Just(yu300), Nothing, ed) → False
new_esEs13(False, True) → False
new_esEs13(True, False) → False
new_esEs21(yu301, yu411001, ty_Ordering) → new_esEs12(yu301, yu411001)
new_esEs24(yu301, yu411001, app(app(ty_@2, bff), bfg)) → new_esEs16(yu301, yu411001, bff, bfg)
new_esEs27(yu300, yu411000, app(ty_Ratio, bhb)) → new_esEs18(yu300, yu411000, bhb)
new_esEs10(Char(yu300), Char(yu411000)) → new_primEqNat0(yu300, yu411000)
new_primEqInt(Pos(Zero), Neg(Succ(yu4110000))) → False
new_primEqInt(Neg(Zero), Pos(Succ(yu4110000))) → False
new_esEs21(yu301, yu411001, ty_@0) → new_esEs19(yu301, yu411001)
new_esEs6(Right(yu300), Right(yu411000), da, ty_Int) → new_esEs8(yu300, yu411000)
new_esEs24(yu301, yu411001, ty_Ordering) → new_esEs12(yu301, yu411001)
new_esEs27(yu300, yu411000, app(ty_Maybe, bgc)) → new_esEs7(yu300, yu411000, bgc)
new_esEs23(yu300, yu411000, ty_Char) → new_esEs10(yu300, yu411000)
new_esEs5(yu31, yu41101, ty_@0) → new_esEs19(yu31, yu41101)
new_esEs6(Left(yu300), Left(yu411000), app(ty_[], cb), bf) → new_esEs15(yu300, yu411000, cb)
new_esEs23(yu300, yu411000, ty_Float) → new_esEs17(yu300, yu411000)
new_esEs7(Just(yu300), Just(yu411000), ty_Double) → new_esEs9(yu300, yu411000)
new_esEs7(Just(yu300), Just(yu411000), app(app(ty_Either, ge), gf)) → new_esEs6(yu300, yu411000, ge, gf)
new_primMulNat0(Zero, Zero) → Zero
new_esEs4(yu30, yu41100, app(ty_Maybe, ed)) → new_esEs7(yu30, yu41100, ed)
new_esEs27(yu300, yu411000, app(app(app(ty_@3, bgd), bge), bgf)) → new_esEs11(yu300, yu411000, bgd, bge, bgf)
new_esEs18(:%(yu300, yu301), :%(yu411000, yu411001), fc) → new_asAs(new_esEs25(yu300, yu411000, fc), new_esEs26(yu301, yu411001, fc))
new_esEs5(yu31, yu41101, app(ty_Ratio, bdd)) → new_esEs18(yu31, yu41101, bdd)
new_esEs4(yu30, yu41100, app(ty_Ratio, fc)) → new_esEs18(yu30, yu41100, fc)
new_esEs21(yu301, yu411001, ty_Integer) → new_esEs14(yu301, yu411001)
new_esEs6(Right(yu300), Right(yu411000), da, app(app(app(ty_@3, dc), dd), de)) → new_esEs11(yu300, yu411000, dc, dd, de)
new_esEs5(yu31, yu41101, ty_Double) → new_esEs9(yu31, yu41101)
new_esEs6(Left(yu300), Left(yu411000), app(app(ty_Either, cf), cg), bf) → new_esEs6(yu300, yu411000, cf, cg)
new_esEs5(yu31, yu41101, app(app(ty_Either, bde), bdf)) → new_esEs6(yu31, yu41101, bde, bdf)
new_esEs24(yu301, yu411001, ty_Double) → new_esEs9(yu301, yu411001)
new_esEs27(yu300, yu411000, app(ty_[], bgg)) → new_esEs15(yu300, yu411000, bgg)
new_primPlusNat0(Zero, yu41100100) → Succ(yu41100100)
new_esEs23(yu300, yu411000, app(app(app(ty_@3, bdh), bea), beb)) → new_esEs11(yu300, yu411000, bdh, bea, beb)
new_esEs23(yu300, yu411000, ty_Double) → new_esEs9(yu300, yu411000)
new_esEs12(EQ, GT) → False
new_esEs12(GT, EQ) → False
new_esEs4(yu30, yu41100, ty_Ordering) → new_esEs12(yu30, yu41100)
new_esEs4(yu30, yu41100, app(app(app(ty_@3, ee), ef), eg)) → new_esEs11(yu30, yu41100, ee, ef, eg)
new_esEs21(yu301, yu411001, app(ty_[], bae)) → new_esEs15(yu301, yu411001, bae)
new_esEs4(yu30, yu41100, app(ty_[], eh)) → new_esEs15(yu30, yu41100, eh)
new_esEs24(yu301, yu411001, app(app(ty_Either, bga), bgb)) → new_esEs6(yu301, yu411001, bga, bgb)
new_esEs24(yu301, yu411001, ty_@0) → new_esEs19(yu301, yu411001)
new_sr(Neg(yu3010), Pos(yu4110010)) → Neg(new_primMulNat0(yu3010, yu4110010))
new_sr(Pos(yu3010), Neg(yu4110010)) → Neg(new_primMulNat0(yu3010, yu4110010))
new_esEs24(yu301, yu411001, ty_Float) → new_esEs17(yu301, yu411001)
new_esEs24(yu301, yu411001, ty_Bool) → new_esEs13(yu301, yu411001)
new_esEs16(@2(yu300, yu301), @2(yu411000, yu411001), fa, fb) → new_asAs(new_esEs23(yu300, yu411000, fa), new_esEs24(yu301, yu411001, fb))
new_esEs6(Left(yu300), Left(yu411000), ty_Bool, bf) → new_esEs13(yu300, yu411000)
new_esEs7(Just(yu300), Just(yu411000), ty_Ordering) → new_esEs12(yu300, yu411000)
new_esEs12(LT, GT) → False
new_esEs12(GT, LT) → False
new_esEs27(yu300, yu411000, app(app(ty_Either, bhc), bhd)) → new_esEs6(yu300, yu411000, bhc, bhd)
new_esEs20(yu300, yu411000, app(app(app(ty_@3, gh), ha), hb)) → new_esEs11(yu300, yu411000, gh, ha, hb)
new_esEs21(yu301, yu411001, app(ty_Maybe, baa)) → new_esEs7(yu301, yu411001, baa)
new_esEs20(yu300, yu411000, ty_Char) → new_esEs10(yu300, yu411000)
new_esEs7(Just(yu300), Just(yu411000), ty_Integer) → new_esEs14(yu300, yu411000)
new_esEs24(yu301, yu411001, ty_Int) → new_esEs8(yu301, yu411001)
new_esEs21(yu301, yu411001, app(app(ty_Either, bba), bbb)) → new_esEs6(yu301, yu411001, bba, bbb)
new_esEs6(Right(yu300), Right(yu411000), da, ty_Bool) → new_esEs13(yu300, yu411000)
new_esEs7(Just(yu300), Just(yu411000), ty_Int) → new_esEs8(yu300, yu411000)
new_esEs4(yu30, yu41100, ty_Float) → new_esEs17(yu30, yu41100)
new_esEs20(yu300, yu411000, app(app(ty_@2, hd), he)) → new_esEs16(yu300, yu411000, hd, he)
new_esEs26(yu301, yu411001, ty_Integer) → new_esEs14(yu301, yu411001)
new_esEs17(Float(yu300, yu301), Float(yu411000, yu411001)) → new_esEs8(new_sr(yu300, yu411000), new_sr(yu301, yu411001))
new_esEs23(yu300, yu411000, ty_Bool) → new_esEs13(yu300, yu411000)
new_esEs21(yu301, yu411001, ty_Char) → new_esEs10(yu301, yu411001)
new_esEs5(yu31, yu41101, ty_Integer) → new_esEs14(yu31, yu41101)
new_esEs22(yu302, yu411002, app(ty_Ratio, bcb)) → new_esEs18(yu302, yu411002, bcb)
new_primEqNat0(Zero, Succ(yu4110000)) → False
new_primEqNat0(Succ(yu3000), Zero) → False
new_esEs22(yu302, yu411002, ty_Float) → new_esEs17(yu302, yu411002)
new_esEs22(yu302, yu411002, ty_Ordering) → new_esEs12(yu302, yu411002)
new_esEs5(yu31, yu41101, ty_Char) → new_esEs10(yu31, yu41101)
new_esEs5(yu31, yu41101, app(ty_Maybe, bce)) → new_esEs7(yu31, yu41101, bce)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs23(yu300, yu411000, app(ty_Ratio, bef)) → new_esEs18(yu300, yu411000, bef)
new_esEs23(yu300, yu411000, ty_@0) → new_esEs19(yu300, yu411000)
new_esEs26(yu301, yu411001, ty_Int) → new_esEs8(yu301, yu411001)
new_esEs20(yu300, yu411000, app(app(ty_Either, hg), hh)) → new_esEs6(yu300, yu411000, hg, hh)
new_esEs5(yu31, yu41101, ty_Ordering) → new_esEs12(yu31, yu41101)
new_esEs7(Just(yu300), Just(yu411000), app(app(ty_@2, gb), gc)) → new_esEs16(yu300, yu411000, gb, gc)
new_esEs27(yu300, yu411000, ty_Float) → new_esEs17(yu300, yu411000)
new_esEs5(yu31, yu41101, ty_Bool) → new_esEs13(yu31, yu41101)
new_esEs24(yu301, yu411001, app(ty_Maybe, bfa)) → new_esEs7(yu301, yu411001, bfa)
new_esEs23(yu300, yu411000, app(ty_Maybe, bdg)) → new_esEs7(yu300, yu411000, bdg)
new_esEs22(yu302, yu411002, app(ty_[], bbg)) → new_esEs15(yu302, yu411002, bbg)
new_esEs6(Left(yu300), Left(yu411000), app(ty_Maybe, be), bf) → new_esEs7(yu300, yu411000, be)
new_esEs25(yu300, yu411000, ty_Integer) → new_esEs14(yu300, yu411000)
new_esEs6(Left(yu300), Left(yu411000), ty_Ordering, bf) → new_esEs12(yu300, yu411000)
new_esEs6(Left(yu300), Left(yu411000), ty_@0, bf) → new_esEs19(yu300, yu411000)
new_esEs14(Integer(yu300), Integer(yu411000)) → new_primEqInt(yu300, yu411000)
new_esEs20(yu300, yu411000, app(ty_Ratio, hf)) → new_esEs18(yu300, yu411000, hf)
new_esEs6(Left(yu300), Left(yu411000), ty_Integer, bf) → new_esEs14(yu300, yu411000)
new_esEs11(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), ee, ef, eg) → new_asAs(new_esEs20(yu300, yu411000, ee), new_asAs(new_esEs21(yu301, yu411001, ef), new_esEs22(yu302, yu411002, eg)))
new_esEs15([], :(yu411000, yu411001), eh) → False
new_esEs15(:(yu300, yu301), [], eh) → False
new_esEs4(yu30, yu41100, ty_Integer) → new_esEs14(yu30, yu41100)
new_esEs7(Just(yu300), Just(yu411000), app(ty_Ratio, gd)) → new_esEs18(yu300, yu411000, gd)
new_esEs6(Left(yu300), Left(yu411000), ty_Double, bf) → new_esEs9(yu300, yu411000)
new_esEs5(yu31, yu41101, ty_Int) → new_esEs8(yu31, yu41101)
new_esEs5(yu31, yu41101, app(app(app(ty_@3, bcf), bcg), bch)) → new_esEs11(yu31, yu41101, bcf, bcg, bch)
new_esEs6(Left(yu300), Right(yu411000), da, bf) → False
new_esEs6(Right(yu300), Left(yu411000), da, bf) → False
new_esEs21(yu301, yu411001, ty_Double) → new_esEs9(yu301, yu411001)
new_esEs21(yu301, yu411001, app(app(ty_@2, baf), bag)) → new_esEs16(yu301, yu411001, baf, bag)
new_sr(Neg(yu3010), Neg(yu4110010)) → Pos(new_primMulNat0(yu3010, yu4110010))
new_esEs12(LT, LT) → True
new_asAs(False, yu103) → False
new_sr(Pos(yu3010), Pos(yu4110010)) → Pos(new_primMulNat0(yu3010, yu4110010))
new_primEqNat0(Zero, Zero) → True
new_esEs27(yu300, yu411000, app(app(ty_@2, bgh), bha)) → new_esEs16(yu300, yu411000, bgh, bha)
new_esEs7(Just(yu300), Just(yu411000), ty_Float) → new_esEs17(yu300, yu411000)
new_primMulNat0(Zero, Succ(yu41100100)) → Zero
new_primMulNat0(Succ(yu30100), Zero) → Zero
new_esEs4(yu30, yu41100, ty_@0) → new_esEs19(yu30, yu41100)
new_esEs4(yu30, yu41100, ty_Int) → new_esEs8(yu30, yu41100)
new_esEs23(yu300, yu411000, app(app(ty_Either, beg), beh)) → new_esEs6(yu300, yu411000, beg, beh)
new_esEs27(yu300, yu411000, ty_Int) → new_esEs8(yu300, yu411000)
new_esEs21(yu301, yu411001, ty_Bool) → new_esEs13(yu301, yu411001)
new_esEs6(Right(yu300), Right(yu411000), da, app(ty_Ratio, ea)) → new_esEs18(yu300, yu411000, ea)
new_esEs23(yu300, yu411000, ty_Ordering) → new_esEs12(yu300, yu411000)
new_esEs15(:(yu300, yu301), :(yu411000, yu411001), eh) → new_asAs(new_esEs27(yu300, yu411000, eh), new_esEs15(yu301, yu411001, eh))
new_esEs20(yu300, yu411000, ty_Bool) → new_esEs13(yu300, yu411000)
new_esEs6(Right(yu300), Right(yu411000), da, app(app(ty_Either, eb), ec)) → new_esEs6(yu300, yu411000, eb, ec)
new_esEs24(yu301, yu411001, ty_Char) → new_esEs10(yu301, yu411001)
new_esEs22(yu302, yu411002, ty_Char) → new_esEs10(yu302, yu411002)
new_esEs6(Right(yu300), Right(yu411000), da, app(ty_[], df)) → new_esEs15(yu300, yu411000, df)
new_esEs4(yu30, yu41100, ty_Double) → new_esEs9(yu30, yu41100)
new_esEs13(False, False) → True
new_esEs20(yu300, yu411000, app(ty_[], hc)) → new_esEs15(yu300, yu411000, hc)
new_esEs23(yu300, yu411000, app(ty_[], bec)) → new_esEs15(yu300, yu411000, bec)
new_esEs6(Right(yu300), Right(yu411000), da, ty_Char) → new_esEs10(yu300, yu411000)
new_esEs4(yu30, yu41100, ty_Bool) → new_esEs13(yu30, yu41100)
new_esEs6(Right(yu300), Right(yu411000), da, ty_Integer) → new_esEs14(yu300, yu411000)
new_esEs22(yu302, yu411002, ty_Double) → new_esEs9(yu302, yu411002)
new_esEs9(Double(yu300, yu301), Double(yu411000, yu411001)) → new_esEs8(new_sr(yu300, yu411000), new_sr(yu301, yu411001))
new_esEs4(yu30, yu41100, app(app(ty_Either, da), bf)) → new_esEs6(yu30, yu41100, da, bf)
new_esEs22(yu302, yu411002, ty_Int) → new_esEs8(yu302, yu411002)
new_primPlusNat0(Succ(yu1040), yu41100100) → Succ(Succ(new_primPlusNat1(yu1040, yu41100100)))
new_esEs27(yu300, yu411000, ty_Char) → new_esEs10(yu300, yu411000)
new_esEs20(yu300, yu411000, ty_Integer) → new_esEs14(yu300, yu411000)
new_esEs6(Right(yu300), Right(yu411000), da, ty_Double) → new_esEs9(yu300, yu411000)
new_esEs24(yu301, yu411001, ty_Integer) → new_esEs14(yu301, yu411001)
new_esEs6(Left(yu300), Left(yu411000), ty_Int, bf) → new_esEs8(yu300, yu411000)
new_primEqInt(Neg(Succ(yu3000)), Neg(Succ(yu4110000))) → new_primEqNat0(yu3000, yu4110000)
new_esEs20(yu300, yu411000, ty_Float) → new_esEs17(yu300, yu411000)
new_esEs5(yu31, yu41101, ty_Float) → new_esEs17(yu31, yu41101)
new_esEs7(Just(yu300), Just(yu411000), ty_@0) → new_esEs19(yu300, yu411000)
new_esEs27(yu300, yu411000, ty_Bool) → new_esEs13(yu300, yu411000)
new_esEs5(yu31, yu41101, app(app(ty_@2, bdb), bdc)) → new_esEs16(yu31, yu41101, bdb, bdc)
new_primPlusNat1(Zero, Succ(yu411001000)) → Succ(yu411001000)
new_primPlusNat1(Succ(yu10400), Zero) → Succ(yu10400)
new_esEs23(yu300, yu411000, app(app(ty_@2, bed), bee)) → new_esEs16(yu300, yu411000, bed, bee)
new_esEs20(yu300, yu411000, ty_Ordering) → new_esEs12(yu300, yu411000)
new_esEs12(LT, EQ) → False
new_esEs12(EQ, LT) → False
new_esEs27(yu300, yu411000, ty_Ordering) → new_esEs12(yu300, yu411000)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs22(yu302, yu411002, app(app(ty_Either, bcc), bcd)) → new_esEs6(yu302, yu411002, bcc, bcd)
new_esEs6(Right(yu300), Right(yu411000), da, app(app(ty_@2, dg), dh)) → new_esEs16(yu300, yu411000, dg, dh)
new_esEs12(GT, GT) → True
new_primEqInt(Neg(Succ(yu3000)), Neg(Zero)) → False
new_primEqInt(Neg(Zero), Neg(Succ(yu4110000))) → False
new_esEs6(Right(yu300), Right(yu411000), da, ty_@0) → new_esEs19(yu300, yu411000)
new_esEs6(Left(yu300), Left(yu411000), ty_Char, bf) → new_esEs10(yu300, yu411000)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs21(yu301, yu411001, ty_Float) → new_esEs17(yu301, yu411001)
new_esEs20(yu300, yu411000, ty_@0) → new_esEs19(yu300, yu411000)
new_esEs19(@0, @0) → True
new_esEs27(yu300, yu411000, ty_Integer) → new_esEs14(yu300, yu411000)
new_esEs20(yu300, yu411000, ty_Int) → new_esEs8(yu300, yu411000)
new_asAs(True, yu103) → yu103
new_esEs23(yu300, yu411000, ty_Integer) → new_esEs14(yu300, yu411000)
new_esEs6(Left(yu300), Left(yu411000), app(ty_Ratio, ce), bf) → new_esEs18(yu300, yu411000, ce)
new_primMulNat0(Succ(yu30100), Succ(yu41100100)) → new_primPlusNat0(new_primMulNat0(yu30100, Succ(yu41100100)), yu41100100)
new_esEs20(yu300, yu411000, ty_Double) → new_esEs9(yu300, yu411000)
new_esEs13(True, True) → True
new_esEs22(yu302, yu411002, ty_@0) → new_esEs19(yu302, yu411002)
new_esEs7(Just(yu300), Just(yu411000), app(app(app(ty_@3, ff), fg), fh)) → new_esEs11(yu300, yu411000, ff, fg, fh)
new_esEs7(Just(yu300), Just(yu411000), ty_Char) → new_esEs10(yu300, yu411000)
new_primEqInt(Pos(Succ(yu3000)), Pos(Succ(yu4110000))) → new_primEqNat0(yu3000, yu4110000)
new_esEs22(yu302, yu411002, ty_Bool) → new_esEs13(yu302, yu411002)
new_esEs22(yu302, yu411002, app(app(app(ty_@3, bbd), bbe), bbf)) → new_esEs11(yu302, yu411002, bbd, bbe, bbf)
new_esEs6(Left(yu300), Left(yu411000), ty_Float, bf) → new_esEs17(yu300, yu411000)
new_esEs24(yu301, yu411001, app(app(app(ty_@3, bfb), bfc), bfd)) → new_esEs11(yu301, yu411001, bfb, bfc, bfd)
new_esEs5(yu31, yu41101, app(ty_[], bda)) → new_esEs15(yu31, yu41101, bda)
new_esEs4(yu30, yu41100, app(app(ty_@2, fa), fb)) → new_esEs16(yu30, yu41100, fa, fb)
new_primEqNat0(Succ(yu3000), Succ(yu4110000)) → new_primEqNat0(yu3000, yu4110000)
new_esEs4(yu30, yu41100, ty_Char) → new_esEs10(yu30, yu41100)
new_esEs7(Just(yu300), Just(yu411000), ty_Bool) → new_esEs13(yu300, yu411000)
new_esEs24(yu301, yu411001, app(ty_Ratio, bfh)) → new_esEs18(yu301, yu411001, bfh)
new_esEs6(Right(yu300), Right(yu411000), da, ty_Ordering) → new_esEs12(yu300, yu411000)
new_esEs21(yu301, yu411001, app(app(app(ty_@3, bab), bac), bad)) → new_esEs11(yu301, yu411001, bab, bac, bad)
new_esEs6(Left(yu300), Left(yu411000), app(app(app(ty_@3, bg), bh), ca), bf) → new_esEs11(yu300, yu411000, bg, bh, ca)
new_esEs12(EQ, EQ) → True
new_esEs7(Nothing, Nothing, ed) → True
new_esEs24(yu301, yu411001, app(ty_[], bfe)) → new_esEs15(yu301, yu411001, bfe)
new_esEs23(yu300, yu411000, ty_Int) → new_esEs8(yu300, yu411000)
new_esEs21(yu301, yu411001, ty_Int) → new_esEs8(yu301, yu411001)
new_esEs15([], [], eh) → True
new_primEqInt(Pos(Succ(yu3000)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Pos(Succ(yu4110000))) → False
new_esEs27(yu300, yu411000, ty_@0) → new_esEs19(yu300, yu411000)
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_esEs22(yu302, yu411002, app(ty_Maybe, bbc)) → new_esEs7(yu302, yu411002, bbc)
new_esEs21(yu301, yu411001, app(ty_Ratio, bah)) → new_esEs18(yu301, yu411001, bah)
new_esEs8(yu30, yu41100) → new_primEqInt(yu30, yu41100)
new_esEs6(Right(yu300), Right(yu411000), da, app(ty_Maybe, db)) → new_esEs7(yu300, yu411000, db)

The set Q consists of the following terms:

new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs6(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_sr(Neg(x0), Neg(x1))
new_esEs20(x0, x1, ty_Bool)
new_esEs7(Just(x0), Just(x1), ty_Int)
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_esEs6(Left(x0), Left(x1), ty_Float, x2)
new_esEs5(x0, x1, app(ty_Ratio, x2))
new_esEs23(x0, x1, ty_Int)
new_esEs5(x0, x1, app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs24(x0, x1, ty_@0)
new_esEs6(Left(x0), Left(x1), app(ty_[], x2), x3)
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_esEs6(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs21(x0, x1, ty_Char)
new_sr(Pos(x0), Pos(x1))
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, ty_Int)
new_asAs(False, x0)
new_esEs6(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs20(x0, x1, ty_Integer)
new_primPlusNat1(Succ(x0), Zero)
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs5(x0, x1, ty_Double)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs27(x0, x1, ty_Bool)
new_esEs23(x0, x1, ty_Integer)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs24(x0, x1, ty_Double)
new_esEs22(x0, x1, ty_@0)
new_esEs20(x0, x1, ty_Int)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs6(Right(x0), Right(x1), x2, ty_Float)
new_esEs6(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs20(x0, x1, app(ty_[], x2))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs27(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, ty_@0)
new_primEqNat0(Zero, Succ(x0))
new_esEs15(:(x0, x1), [], x2)
new_esEs4(x0, x1, ty_Double)
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, ty_Double)
new_asAs(True, x0)
new_esEs27(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs27(x0, x1, ty_Char)
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_esEs12(GT, EQ)
new_esEs12(EQ, GT)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs6(Right(x0), Right(x1), x2, ty_Char)
new_esEs23(x0, x1, ty_Double)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs6(Right(x0), Right(x1), x2, ty_Double)
new_esEs20(x0, x1, ty_Ordering)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs16(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs5(x0, x1, ty_Float)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs12(GT, GT)
new_esEs4(x0, x1, ty_Float)
new_esEs4(x0, x1, ty_Integer)
new_esEs6(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs22(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_Bool)
new_esEs4(x0, x1, ty_Bool)
new_esEs21(x0, x1, ty_Double)
new_esEs6(Left(x0), Left(x1), ty_Int, x2)
new_esEs6(Right(x0), Right(x1), x2, ty_@0)
new_esEs22(x0, x1, ty_Float)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs7(Just(x0), Just(x1), ty_@0)
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs24(x0, x1, ty_Float)
new_esEs14(Integer(x0), Integer(x1))
new_esEs24(x0, x1, ty_Char)
new_primMulNat0(Zero, Succ(x0))
new_esEs8(x0, x1)
new_esEs5(x0, x1, ty_Integer)
new_primPlusNat0(Succ(x0), x1)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs7(Just(x0), Just(x1), ty_Char)
new_esEs7(Nothing, Nothing, x0)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, ty_Ordering)
new_esEs7(Just(x0), Just(x1), ty_Bool)
new_primEqNat0(Zero, Zero)
new_esEs4(x0, x1, ty_Ordering)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs5(x0, x1, ty_Bool)
new_esEs22(x0, x1, ty_Int)
new_esEs23(x0, x1, ty_Ordering)
new_primEqNat0(Succ(x0), Zero)
new_esEs6(Left(x0), Left(x1), ty_Bool, x2)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs27(x0, x1, ty_Ordering)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primPlusNat1(Zero, Succ(x0))
new_esEs6(Left(x0), Left(x1), ty_Double, x2)
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Float)
new_primMulNat0(Zero, Zero)
new_esEs13(False, False)
new_esEs5(x0, x1, ty_Int)
new_esEs5(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, ty_Float)
new_esEs7(Just(x0), Just(x1), ty_Integer)
new_esEs6(Right(x0), Right(x1), x2, ty_Int)
new_esEs26(x0, x1, ty_Int)
new_esEs13(False, True)
new_esEs13(True, False)
new_esEs5(x0, x1, ty_Char)
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs7(Just(x0), Just(x1), ty_Ordering)
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs22(x0, x1, ty_Double)
new_esEs7(Just(x0), Just(x1), ty_Float)
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs15([], [], x0)
new_primMulNat0(Succ(x0), Zero)
new_esEs6(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs4(x0, x1, ty_Char)
new_esEs7(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs11(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs4(x0, x1, ty_Int)
new_esEs13(True, True)
new_esEs7(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs27(x0, x1, app(ty_Maybe, x2))
new_esEs5(x0, x1, app(ty_[], x2))
new_esEs15([], :(x0, x1), x2)
new_esEs27(x0, x1, ty_Integer)
new_esEs7(Nothing, Just(x0), x1)
new_esEs6(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs6(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs27(x0, x1, app(ty_Ratio, x2))
new_esEs5(x0, x1, app(ty_Maybe, x2))
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs15(:(x0, x1), :(x2, x3), x4)
new_esEs27(x0, x1, app(app(ty_@2, x2), x3))
new_esEs4(x0, x1, ty_@0)
new_esEs6(Left(x0), Left(x1), ty_@0, x2)
new_esEs21(x0, x1, ty_Bool)
new_esEs6(Right(x0), Left(x1), x2, x3)
new_esEs6(Left(x0), Right(x1), x2, x3)
new_esEs23(x0, x1, ty_Bool)
new_esEs7(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs18(:%(x0, x1), :%(x2, x3), x4)
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6(Right(x0), Right(x1), x2, ty_Bool)
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_esEs23(x0, x1, ty_Float)
new_esEs27(x0, x1, ty_Float)
new_esEs23(x0, x1, ty_@0)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs6(Left(x0), Left(x1), ty_Char, x2)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs25(x0, x1, ty_Integer)
new_esEs21(x0, x1, ty_Integer)
new_esEs6(Right(x0), Right(x1), x2, ty_Integer)
new_esEs6(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs6(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs27(x0, x1, app(app(ty_Either, x2), x3))
new_esEs12(EQ, LT)
new_esEs12(LT, EQ)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs7(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs6(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, ty_Char)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs9(Double(x0, x1), Double(x2, x3))
new_primPlusNat1(Zero, Zero)
new_esEs25(x0, x1, ty_Int)
new_esEs12(EQ, EQ)
new_esEs6(Left(x0), Left(x1), ty_Integer, x2)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs7(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs7(Just(x0), Just(x1), app(ty_[], x2))
new_esEs24(x0, x1, ty_Integer)
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs7(Just(x0), Nothing, x1)
new_primPlusNat0(Zero, x0)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs10(Char(x0), Char(x1))
new_esEs21(x0, x1, ty_Ordering)
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs17(Float(x0, x1), Float(x2, x3))
new_esEs24(x0, x1, ty_Bool)
new_esEs22(x0, x1, ty_Ordering)
new_esEs5(x0, x1, ty_@0)
new_esEs5(x0, x1, app(app(ty_Either, x2), x3))
new_esEs27(x0, x1, ty_Int)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs5(x0, x1, ty_Ordering)
new_esEs7(Just(x0), Just(x1), ty_Double)
new_esEs19(@0, @0)
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_esEs26(x0, x1, ty_Integer)
new_esEs27(x0, x1, ty_@0)
new_esEs27(x0, x1, ty_Double)
new_esEs20(x0, x1, ty_Char)
new_esEs12(LT, LT)
new_esEs24(x0, x1, ty_Int)
new_esEs12(LT, GT)
new_esEs12(GT, LT)
new_esEs6(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs22(x0, x1, ty_Char)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs21(x0, x1, ty_@0)
new_esEs6(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: